es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, Q:({e:E| loc(e) = loc(e1)  Id }Prop).
[e1,e2]~([a,b].e[a,b].Q(e))+  e1  e2  & e[e1,e2].Q(e) 

latex

Definitions

t  T, x:A. B(x), loc(e), Id, E, b, P  Q, False, A, x(s), Prop, x. t(x), e[e1,e2].P(e), x,y. t(x;y), [e1,e2]~([a,b].p(a;b))+, e  e' , P & Q, P  Q, (e <loc e'), P  Q, P  Q, ES, , x:A. B(x), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), first(e), {i..j}, 1of(t), AB, i  j < k, [e, e'], upto(n), pred(e), map(f;as), concat(ll), as @ bs, {T}, SQType(T), Dec(P), True, T, S  T, S  T, ij, , Top, i=j, b, , Unit, (x  l)

Lemmas

member map, member-concat, member append, concat wf, l member wf, member-es-interval, es-le-pred, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, map append sq, concat append, map wf, upto wf, concat-cons, concat-nil, append-nil, es-interval wf2, top wf, es-pred wf, ge wf, nat properties, nat wf, append wf, es-locl wf, es-interval-partition, es-increasing-sequence, es-interval wf, squash wf, true wf, decidable int equal, int seg wf, es-locl-iff, le wf, int seg properties, nat plus properties, event system wf, es-pplus wf, es-le wf, es-pplus-le, es-pplus-trivial, alle-between2 wf, es-le-loc, es-loc-pred, es-E wf, Id wf, es-loc wf